|
In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem states necessary and sufficient conditions under which a finite set ''S'' of relations over the Boolean domain yields polynomial-time or NP-complete problems when the relations of ''S'' are used to constrain some of the propositional variables.〔 〕 It is called a dichotomy theorem because the complexity of the problem defined by ''S'' is either in P or NP-complete as opposed to one of the classes of intermediate complexity that is known to exist (assuming P ≠ NP) by Ladner's theorem. Special cases of Schaefer's dichotomy theorem include the NP-completeness of SAT (the Boolean satisfiability problem) and its two popular variants 1-in-3 SAT and Not-All-Equal 3SAT (often denoted by NAE-3SAT). In fact, for these two variants of SAT, Schaefer's dichotomy theorem shows that their monotone versions (where negations of variables are not allowed) are also NP-complete. == Original presentation == Schaefer defines a decision problem that he calls the Generalized Satisfiability problem for ''S'' (denoted by SAT(''S'')). An instance of the problem is an ''S''-formula, i.e. a conjunction of constraints of the form where R is a relation in ''S'' and the are propositional variables. The problem is to determine whether the given formula is satisfiable, in other words if the variables can be assigned values such that they satisfy all the constraints. Schaefer identifies six classes of sets of Boolean relations for which SAT(''S'') is in P and proves that all other sets of relations generate an NP-complete problem. A finite set of relations ''S'' over the Boolean domain defines a polynomial time computable satisfiability problem if any one of the following conditions holds: # all relations which are not constantly false are true when all its arguments are true; # all relations which are not constantly false are true when all its arguments are false; # all relations are equivalent to a conjunction of binary clauses; # all relations are equivalent to a conjunction of Horn clauses; # all relations are equivalent to a conjunction of dual-Horn clauses; # all relations are equivalent to a conjunction of affine formulae. 〔Schaefer (1978, p.218 left) defines an affine formula to be of the form ''x''1 ⊕ ... ⊕ ''x''''n'' = ''c'', where each ''x''''i'' is a variable, ''c'' is a constant, i.e. ''true'' or ''false'', and "⊕" denotes XOR, i.e. addition in a Boolean ring.〕 Otherwise, the problem SAT(''S'') is NP-complete. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Schaefer's dichotomy theorem」の詳細全文を読む スポンサード リンク
|